/-
Copyright (c) 2023 Kim Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kim Morrison
-/
module

public import Mathlib.Algebra.Group.Submonoid.Operations
public import Mathlib.Algebra.GroupWithZero.Regular
public import Mathlib.Algebra.Order.Module.Defs
public import Mathlib.Algebra.Order.Group.Nat
public import Mathlib.Algebra.Order.Group.Opposite
public import Mathlib.Algebra.Star.SelfAdjoint
public import Mathlib.Algebra.Star.StarRingHom
public import Mathlib.Tactic.ContinuousFunctionalCalculus
public import Mathlib.Algebra.Star.StarProjection

/-! # Star ordered rings

We define the class `StarOrderedRing R`, which says that the order on `R` respects the
star operation, i.e. an element `r` is nonnegative iff it is in the `AddSubmonoid` generated by
elements of the form `star s * s`. In many cases, including all C⋆-algebras, this can be reduced to
`0 ≤ r ↔ ∃ s, r = star s * s`. However, this generality is slightly more convenient (e.g., it
allows us to register a `StarOrderedRing` instance for `ℚ`), and more closely resembles the
literature (see the seminal paper [*The positive cone in Banach algebras*][kelleyVaught1953])

In order to accommodate `NonUnitalSemiring R`, we actually don't characterize nonnegativity, but
rather the entire `≤` relation with `StarOrderedRing.le_iff`. However, notice that when `R` is a
`NonUnitalRing`, these are equivalent (see `StarOrderedRing.nonneg_iff` and
`StarOrderedRing.of_nonneg_iff`).

It is important to note that while a `StarOrderedRing` is an `OrderedAddCommMonoid` it is often
*not* an `OrderedSemiring`.

## TODO

* In a Banach star algebra without a well-defined square root, the natural ordering is given by the
  positive cone which is the _closure_ of the sums of elements `star r * r`. A weaker version of
  `StarOrderedRing` could be defined for this case (again, see
  [*The positive cone in Banach algebras*][kelleyVaught1953]). Note that the current definition has
  the advantage of not requiring a topology.
-/

@[expose] public section

open Set
open scoped NNRat

variable {R A : Type*}

section prereq
variable [Semiring R] [StarRing R]
  [NonUnitalSemiring A] [StarRing A] [Module R A]
  [StarModule R A] [IsScalarTower R A A] [SMulCommClass R A A]

lemma smul_mem_closure_star_mul {r : R}
    (hr : r ∈ AddSubmonoid.closure (range fun s ↦ star s * s)) {a : A}
    (ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)) :
    r • a ∈ AddSubmonoid.closure (range fun s ↦ star s * s) := by
  induction hr using AddSubmonoid.closure_induction with
  | zero => simp
  | add r₁ r₂ _ _ hr₁ hr₂ => simpa [add_smul] using add_mem hr₁ hr₂
  | mem r hr =>
  induction ha using AddSubmonoid.closure_induction with
  | zero => simp
  | add a₁ a₂ _ _ ha₁ ha₂ => simpa [smul_add] using add_mem ha₁ ha₂
  | mem a ha =>
  obtain ⟨r, rfl⟩ := hr
  obtain ⟨a, rfl⟩ := ha
  exact AddSubmonoid.subset_closure ⟨r • a, by simp [star_smul, smul_mul_smul_comm]⟩

end prereq

/-- An ordered `*`-ring is a `*`-ring with a partial order such that the nonnegative elements
constitute precisely the `AddSubmonoid` generated by elements of the form `star s * s`.

If you are working with a `NonUnitalRing` and not a `NonUnitalSemiring`, it may be more
convenient to declare instances using `StarOrderedRing.of_nonneg_iff`. -/
class StarOrderedRing (R : Type*) [NonUnitalSemiring R] [PartialOrder R] [StarRing R] : Prop where
  /-- characterization of the order in terms of the `StarRing` structure. -/
  le_iff :
    ∀ x y : R, x ≤ y ↔ ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + p

namespace StarOrderedRing
section NonUnitalSemiring
variable [NonUnitalSemiring R] [PartialOrder R] [StarRing R]

/-- To construct a `StarOrderedRing` instance it suffices to show that `x ≤ y` if and only if
`y = x + star s * s` for some `s : R`.

This is provided for convenience because it holds in some common scenarios (e.g.,`ℝ≥0`, `C(X, ℝ≥0)`)
and obviates the hassle of `AddSubmonoid.closure_induction` when creating those instances.

If you are working with a `NonUnitalRing` and not a `NonUnitalSemiring`, see
`StarOrderedRing.of_nonneg_iff` for a more convenient version.
-/
lemma of_le_iff (h_le_iff : ∀ x y : R, x ≤ y ↔ ∃ s, y = x + star s * s) : StarOrderedRing R where
  le_iff x y := by
    refine ⟨fun h => ?_, ?_⟩
    · obtain ⟨p, hp⟩ := (h_le_iff x y).mp h
      exact ⟨star p * p, AddSubmonoid.subset_closure ⟨p, rfl⟩, hp⟩
    · rintro ⟨p, hp, hpxy⟩
      revert x y hpxy
      refine AddSubmonoid.closure_induction ?_ (fun x y h => add_zero x ▸ h.ge) ?_ hp
      · rintro _ ⟨s, rfl⟩ x y rfl
        exact (h_le_iff _ _).mpr ⟨s, rfl⟩
      · rintro _ _ _ _ ha hb x y rfl
        rw [← add_assoc]
        exact (ha _ _ rfl).trans (hb _ _ rfl)

variable [StarOrderedRing R] {x y : R}

-- see note [lower instance priority]
instance (priority := 100) toIsOrderedAddMonoid : IsOrderedAddMonoid R where
  add_le_add_left := fun x y hle z ↦ by
    rw [StarOrderedRing.le_iff] at hle ⊢
    refine hle.imp fun s hs ↦ ?_
    rw [hs.2, add_right_comm]
    exact ⟨hs.1, rfl⟩

-- see note [lower instance priority]
instance (priority := 100) toExistsAddOfLE : ExistsAddOfLE R where
  exists_add_of_le h :=
    match (le_iff _ _).mp h with
    | ⟨p, _, hp⟩ => ⟨p, hp⟩

lemma nonneg_iff : 0 ≤ x ↔ x ∈ AddSubmonoid.closure (Set.range fun s : R => star s * s) := by
  simp only [le_iff, zero_add, exists_eq_right']

lemma pos_iff : 0 < x ↔ x ≠ 0 ∧ x ∈ AddSubmonoid.closure (Set.range fun s : R => star s * s) := by
  simp [lt_iff_le_and_ne, and_comm, eq_comm, le_iff]

variable [IsCancelAdd R]

lemma lt_iff :
    x < y ↔ ∃ p ≠ 0, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + p := by
  rw [lt_iff_le_and_ne, and_comm, StarOrderedRing.le_iff, ← exists_and_left]
  congr! 2 with p
  simp +contextual [← and_assoc]

end NonUnitalSemiring

/-- When `R` is a non-unital ring, to construct a `StarOrderedRing` instance it suffices to
show that the nonnegative elements are precisely those elements in the `AddSubmonoid` generated
by `star s * s` for `s : R`. -/
lemma of_nonneg_iff [NonUnitalRing R] [PartialOrder R] [StarRing R]
    (h_add : ∀ {x y : R}, x ≤ y → ∀ z, z + x ≤ z + y)
    (h_nonneg_iff : ∀ x : R, 0 ≤ x ↔ x ∈ AddSubmonoid.closure (Set.range fun s : R => star s * s)) :
    StarOrderedRing R where
  le_iff x y := by
    have : AddLeftMono R := ⟨fun _ _ _ h => h_add h _⟩
    simpa only [← sub_eq_iff_eq_add', sub_nonneg, exists_eq_right'] using h_nonneg_iff (y - x)

/-- When `R` is a non-unital ring, to construct a `StarOrderedRing` instance it suffices to
show that the nonnegative elements are precisely those elements of the form `star s * s`
for `s : R`.

This is provided for convenience because it holds in many common scenarios (e.g.,`ℝ`, `ℂ`, or
any C⋆-algebra), and obviates the hassle of `AddSubmonoid.closure_induction` when creating those
instances. -/
lemma of_nonneg_iff' [NonUnitalRing R] [PartialOrder R] [StarRing R]
    (h_add : ∀ {x y : R}, x ≤ y → ∀ z, z + x ≤ z + y)
    (h_nonneg_iff : ∀ x : R, 0 ≤ x ↔ ∃ s, x = star s * s) : StarOrderedRing R :=
  of_le_iff <| by
    have : AddLeftMono R := ⟨fun _ _ _ h => h_add h _⟩
    simpa [sub_eq_iff_eq_add', sub_nonneg] using fun x y => h_nonneg_iff (y - x)

end StarOrderedRing

section NonUnitalSemiring

variable [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R]

lemma IsSelfAdjoint.mono {x y : R} (h : x ≤ y) (hx : IsSelfAdjoint x) : IsSelfAdjoint y := by
  rw [StarOrderedRing.le_iff] at h
  obtain ⟨d, hd, rfl⟩ := h
  rw [IsSelfAdjoint, star_add, hx.star_eq]
  congr
  refine AddMonoidHom.eqOn_closureM (f := starAddEquiv (R := R)) (g := .id R) ?_ hd
  rintro - ⟨s, rfl⟩
  simp

@[aesop 10% apply]
lemma IsSelfAdjoint.of_nonneg {x : R} (hx : 0 ≤ x) : IsSelfAdjoint x :=
  .mono hx <| .zero R

/-- An alias of `IsSelfAdjoint.of_nonneg` for use with dot notation. -/
alias LE.le.isSelfAdjoint := IsSelfAdjoint.of_nonneg

/-- The combination `(IsSelfAdjoint.star_eq <| .of_nonneg ·)` for use with dot notation. -/
lemma LE.le.star_eq {x : R} (hx : 0 ≤ x) : star x = x :=
  hx.isSelfAdjoint.star_eq

@[simp]
theorem star_mul_self_nonneg (r : R) : 0 ≤ star r * r :=
  StarOrderedRing.nonneg_iff.mpr <| AddSubmonoid.subset_closure ⟨r, rfl⟩

@[simp]
theorem mul_star_self_nonneg (r : R) : 0 ≤ r * star r := by
  simpa only [star_star] using star_mul_self_nonneg (star r)

@[aesop safe apply (rule_sets := [CStarAlgebra])]
protected theorem IsSelfAdjoint.mul_self_nonneg {a : R} (ha : IsSelfAdjoint a) : 0 ≤ a * a := by
  simpa [ha.star_eq] using star_mul_self_nonneg a

/-- A star projection is non-negative in a star-ordered ring. -/
theorem IsStarProjection.nonneg {p : R} (hp : IsStarProjection p) : 0 ≤ p :=
  hp.isIdempotentElem ▸ hp.isSelfAdjoint.mul_self_nonneg

@[aesop safe apply]
theorem star_left_conjugate_nonneg {a : R} (ha : 0 ≤ a) (c : R) : 0 ≤ star c * a * c := by
  rw [StarOrderedRing.nonneg_iff] at ha
  refine AddSubmonoid.closure_induction (fun x hx => ?_)
    (by rw [mul_zero, zero_mul]) (fun x y _ _ hx hy => ?_) ha
  · obtain ⟨x, rfl⟩ := hx
    convert star_mul_self_nonneg (x * c) using 1
    rw [star_mul, ← mul_assoc, mul_assoc _ _ c]
  · calc
      0 ≤ star c * x * c + 0 := by rw [add_zero]; exact hx
      _ ≤ star c * x * c + star c * y * c := by gcongr
      _ ≤ _ := by rw [mul_add, add_mul]

@[deprecated (since := "2025-10-20")] alias conjugate_nonneg :=
  star_left_conjugate_nonneg

@[aesop safe apply]
theorem star_right_conjugate_nonneg {a : R} (ha : 0 ≤ a) (c : R) : 0 ≤ c * a * star c := by
  simpa only [star_star] using star_left_conjugate_nonneg ha (star c)

@[deprecated (since := "2025-10-20")] alias conjugate_nonneg' :=
  star_right_conjugate_nonneg

@[aesop 90% apply (rule_sets := [CStarAlgebra])]
protected theorem IsSelfAdjoint.conjugate_nonneg {a : R} (ha : 0 ≤ a) {c : R}
    (hc : IsSelfAdjoint c) : 0 ≤ c * a * c := by
  nth_rewrite 2 [← hc]; exact star_right_conjugate_nonneg ha c

theorem conjugate_nonneg_of_nonneg {a : R} (ha : 0 ≤ a) {c : R} (hc : 0 ≤ c) :
    0 ≤ c * a * c :=
  IsSelfAdjoint.of_nonneg hc |>.conjugate_nonneg ha

theorem star_left_conjugate_le_conjugate {a b : R} (hab : a ≤ b) (c : R) :
    star c * a * c ≤ star c * b * c := by
  rw [StarOrderedRing.le_iff] at hab ⊢
  obtain ⟨p, hp, rfl⟩ := hab
  simp_rw [← StarOrderedRing.nonneg_iff] at hp ⊢
  exact ⟨star c * p * c, star_left_conjugate_nonneg hp c, by simp only [add_mul, mul_add]⟩

@[deprecated (since := "2025-10-20")] alias conjugate_le_conjugate :=
  star_left_conjugate_le_conjugate

theorem star_right_conjugate_le_conjugate {a b : R} (hab : a ≤ b) (c : R) :
    c * a * star c ≤ c * b * star c := by
  simpa only [star_star] using star_left_conjugate_le_conjugate hab (star c)

@[deprecated (since := "2025-10-20")] alias conjugate_le_conjugate' :=
  star_right_conjugate_le_conjugate

protected theorem IsSelfAdjoint.conjugate_le_conjugate {a b : R} (hab : a ≤ b) {c : R}
    (hc : IsSelfAdjoint c) : c * a * c ≤ c * b * c := by
  simpa only [hc.star_eq] using star_left_conjugate_le_conjugate hab c

theorem conjugate_le_conjugate_of_nonneg {a b : R} (hab : a ≤ b) {c : R} (hc : 0 ≤ c) :
    c * a * c ≤ c * b * c :=
  IsSelfAdjoint.of_nonneg hc |>.conjugate_le_conjugate hab

@[simp]
lemma star_le_star_iff {x y : R} : star x ≤ star y ↔ x ≤ y := by
  suffices ∀ x y, x ≤ y → star x ≤ star y from
    ⟨by simpa only [star_star] using this (star x) (star y), this x y⟩
  intro x y h
  rw [StarOrderedRing.le_iff] at h ⊢
  obtain ⟨d, hd, rfl⟩ := h
  refine ⟨starAddEquiv d, ?_, star_add _ _⟩
  refine AddMonoidHom.mclosure_preimage_le _ _ <| AddSubmonoid.closure_mono ?_ hd
  rintro - ⟨s, rfl⟩
  exact ⟨s, by simp⟩

@[simp]
lemma star_lt_star_iff {x y : R} : star x < star y ↔ x < y := by
  by_cases h : x = y
  · simp [h]
  · simpa [le_iff_lt_or_eq, h] using star_le_star_iff (x := x) (y := y)

lemma star_le_iff {x y : R} : star x ≤ y ↔ x ≤ star y := by rw [← star_le_star_iff, star_star]

lemma star_lt_iff {x y : R} : star x < y ↔ x < star y := by rw [← star_lt_star_iff, star_star]

@[simp]
lemma star_nonneg_iff {x : R} : 0 ≤ star x ↔ 0 ≤ x := by
  simpa using star_le_star_iff (x := 0) (y := x)

@[simp]
lemma star_nonpos_iff {x : R} : star x ≤ 0 ↔ x ≤ 0 := by
  simpa using star_le_star_iff (x := x) (y := 0)

@[simp]
lemma star_pos_iff {x : R} : 0 < star x ↔ 0 < x := by
  simpa using star_lt_star_iff (x := 0) (y := x)

@[simp]
lemma star_neg_iff {x : R} : star x < 0 ↔ x < 0 := by
  simpa using star_lt_star_iff (x := x) (y := 0)

theorem star_left_conjugate_lt_conjugate {a b : R} (hab : a < b) {c : R} (hc : IsRegular c) :
    star c * a * c < star c * b * c := by
  rw [(star_left_conjugate_le_conjugate hab.le _).lt_iff_ne, hc.right.ne_iff, hc.star.left.ne_iff]
  exact hab.ne

@[deprecated (since := "2025-10-20")] alias conjugate_lt_conjugate :=
  star_left_conjugate_lt_conjugate

theorem star_right_conjugate_lt_conjugate {a b : R} (hab : a < b) {c : R} (hc : IsRegular c) :
    c * a * star c < c * b * star c := by
  simpa only [star_star] using star_left_conjugate_lt_conjugate hab hc.star

@[deprecated (since := "2025-10-20")] alias conjugate_lt_conjugate' :=
  star_right_conjugate_lt_conjugate

theorem star_left_conjugate_pos {a : R} (ha : 0 < a) {c : R} (hc : IsRegular c) :
    0 < star c * a * c := by
  simpa only [mul_zero, zero_mul] using star_left_conjugate_lt_conjugate ha hc

@[deprecated (since := "2025-10-20")] alias conjugate_pos := star_left_conjugate_pos

theorem star_right_conjugate_pos {a : R} (ha : 0 < a) {c : R} (hc : IsRegular c) :
    0 < c * a * star c := by
  simpa only [star_star] using star_left_conjugate_pos ha hc.star

@[deprecated (since := "2025-10-20")] alias conjugate_pos' := star_right_conjugate_pos

theorem star_mul_self_pos [Nontrivial R] {x : R} (hx : IsRegular x) : 0 < star x * x := by
  rw [(star_mul_self_nonneg _).lt_iff_ne, ← mul_zero (star x), hx.star.left.ne_iff]
  exact hx.ne_zero.symm

theorem mul_star_self_pos [Nontrivial R] {x : R} (hx : IsRegular x) : 0 < x * star x := by
  simpa using star_mul_self_pos hx.star

end NonUnitalSemiring

section Semiring
variable [Semiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R]

instance : ZeroLEOneClass R where
  zero_le_one := by simpa using star_mul_self_nonneg (1 : R)

@[simp]
lemma one_le_star_iff {x : R} : 1 ≤ star x ↔ 1 ≤ x := by
  simpa using star_le_star_iff (x := 1) (y := x)

@[simp]
lemma star_le_one_iff {x : R} : star x ≤ 1 ↔ x ≤ 1 := by
  simpa using star_le_star_iff (x := x) (y := 1)

@[simp]
lemma one_lt_star_iff {x : R} : 1 < star x ↔ 1 < x := by
  simpa using star_lt_star_iff (x := 1) (y := x)

@[simp]
lemma star_lt_one_iff {x : R} : star x < 1 ↔ x < 1 := by
  simpa using star_lt_star_iff (x := x) (y := 1)

@[aesop safe apply (rule_sets := [CStarAlgebra])]
protected theorem IsSelfAdjoint.sq_nonneg {a : R} (ha : IsSelfAdjoint a) : 0 ≤ a ^ 2 := by
  simp [sq, ha.mul_self_nonneg]

lemma IsUnit.star_right_conjugate_nonneg_iff {u x : R} (hu : IsUnit u) :
    0 ≤ u * x * star u ↔ 0 ≤ x := by
  refine ⟨fun h ↦ ?_, fun h ↦ star_right_conjugate_nonneg h _⟩
  obtain ⟨v, hv⟩ := hu.exists_left_inv
  have := by simpa [← mul_assoc] using star_right_conjugate_nonneg h v
  rwa [hv, one_mul, mul_assoc, ← star_mul, hv, star_one, mul_one] at this

lemma IsUnit.star_left_conjugate_nonneg_iff {u x : R} (hu : IsUnit u) :
    0 ≤ star u * x * u ↔ 0 ≤ x := by
  simpa using hu.star.star_right_conjugate_nonneg_iff

end Semiring

namespace MulOpposite

instance [NonUnitalSemiring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] :
    StarOrderedRing Rᵐᵒᵖ where
  le_iff x y := by
    rw [← unop_le_unop, StarOrderedRing.le_iff, op_surjective.exists,
      ← (AddSubmonoid.closure _).comap_map_eq_of_injective opAddEquiv.injective]
    congr! with p
    · simp [AddMonoidHom.map_mclosure, ← range_comp', Function.comp_def,
        ← (star_involutive.surjective.comp op_surjective).range_comp]
    · simp [← op_inj (α := R)]

end MulOpposite

section StarModule

variable [Semiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R]
  [NonUnitalSemiring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Module R A]
  [StarModule R A] [IsScalarTower R A A] [SMulCommClass R A A]

instance : IsOrderedModule R A where
  smul_le_smul_of_nonneg_left r hr a b hab := by
    rw [StarOrderedRing.nonneg_iff] at hr
    rw [StarOrderedRing.le_iff] at hab ⊢
    obtain ⟨a, ha, rfl⟩ := hab
    exact ⟨r • a, smul_mem_closure_star_mul hr ha, smul_add ..⟩
  smul_le_smul_of_nonneg_right a ha r s hrs := by
    rw [StarOrderedRing.nonneg_iff] at ha
    rw [StarOrderedRing.le_iff] at hrs ⊢
    obtain ⟨r, hr, rfl⟩ := hrs
    exact ⟨r • a, smul_mem_closure_star_mul hr ha, add_smul ..⟩

variable [IsCancelAdd A] [NoZeroSMulDivisors R A]

instance : PosSMulStrictMono R A where
  smul_lt_smul_of_pos_left r hr a b hab := by
    rw [StarOrderedRing.pos_iff] at hr
    rw [StarOrderedRing.lt_iff] at hab ⊢
    obtain ⟨a, ha₀, ha, rfl⟩ := hab
    obtain ⟨hr₀, hr⟩ := hr
    exact ⟨r • a, smul_ne_zero hr₀ ha₀, smul_mem_closure_star_mul hr ha, smul_add ..⟩

instance [IsCancelAdd R] : IsStrictOrderedModule R A where
  smul_lt_smul_of_pos_right a ha r s hrs := by
    rw [StarOrderedRing.pos_iff] at ha
    rw [StarOrderedRing.lt_iff] at hrs ⊢
    obtain ⟨r, hr₀, hr, rfl⟩ := hrs
    obtain ⟨ha₀, ha⟩ := ha
    exact ⟨r • a, smul_ne_zero hr₀ ha₀, smul_mem_closure_star_mul hr ha, add_smul ..⟩

@[deprecated smul_lt_smul_of_pos_left (since := "2025-08-24")]
lemma StarModule.smul_lt_smul_of_pos {a b : A} {c : R} (hab : a < b)
    (hc : 0 < c) : c • a < c • b := smul_lt_smul_of_pos_left hab hc

end StarModule

section OrderClass

variable {F R S : Type*} [NonUnitalSemiring R] [PartialOrder R] [StarRing R]
  [StarOrderedRing R]
variable [NonUnitalSemiring S] [PartialOrder S] [StarRing S] [StarOrderedRing S]

-- we prove this auxiliary lemma in order to avoid duplicating the proof twice below.
lemma NonUnitalStarRingHom.map_le_map_of_map_star (f : R →⋆ₙ+* S) {x y : R} (hxy : x ≤ y) :
    f x ≤ f y := by
  rw [StarOrderedRing.le_iff] at hxy ⊢
  obtain ⟨p, hp, rfl⟩ := hxy
  refine ⟨f p, ?_, map_add f _ _⟩
  have hf : ∀ r, f (star r) = star (f r) := map_star _
  induction hp using AddSubmonoid.closure_induction
  all_goals aesop

instance (priority := 100) StarRingHomClass.instOrderHomClass [FunLike F R S]
    [NonUnitalSemiring R] [StarRing R] [StarOrderedRing R] [NonUnitalSemiring S]
    [StarRing S] [StarOrderedRing S] [NonUnitalRingHomClass F R S]
    [NonUnitalStarRingHomClass F R S] : OrderHomClass F R S where
  map_rel f := (f : R →⋆ₙ+* S).map_le_map_of_map_star

instance (priority := 100) StarRingEquivClass.instOrderIsoClass [EquivLike F R S]
    [StarRingEquivClass F R S] : OrderIsoClass F R S where
  map_le_map_iff f x y := by
    refine ⟨fun h ↦ ?_, map_rel f⟩
    let f_inv : S →⋆ₙ+* R := (f : R ≃⋆+* S).symm
    have f_inv_f (r : R) : f_inv (f r) = r := EquivLike.inv_apply_apply f r
    rw [← f_inv_f x, ← f_inv_f y]
    exact NonUnitalStarRingHom.map_le_map_of_map_star f_inv h

end OrderClass

instance Nat.instStarOrderedRing : StarOrderedRing ℕ where
  le_iff a b := by
    have : AddSubmonoid.closure (range fun x : ℕ ↦ x * x) = ⊤ :=
      eq_top_mono
        (AddSubmonoid.closure_mono <| singleton_subset_iff.2 <| mem_range.2 ⟨1, one_mul _⟩)
        Nat.addSubmonoidClosure_one
    simp [this, le_iff_exists_add]

namespace IsStarProjection

section Ring
variable [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {p : R}

theorem one_sub_nonneg (hp : IsStarProjection p) : 0 ≤ 1 - p := hp.one_sub.nonneg

theorem le_one (hp : IsStarProjection p) : p ≤ 1 := sub_nonneg.mp hp.one_sub_nonneg

/-- For a star projection `p`, we have `0 ≤ p ≤ 1`. -/
theorem mem_Icc (hp : IsStarProjection p) : p ∈ Set.Icc (0 : R) 1 := by
  simp only [Set.mem_Icc, hp.nonneg, hp.le_one, and_self]

end Ring

section NonUnitalRing
variable [NonUnitalRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {p q : R}

/-- A star projection `p` is less than or equal to a star projection `q` when `p * q = p`. -/
theorem le_of_mul_eq_left (hp : IsStarProjection p) (hq : IsStarProjection q)
    (hpq : p * q = p) : p ≤ q := sub_nonneg.mp (hp.sub_of_mul_eq_left hq hpq).nonneg

/-- A star projection `p` is less than or equal to a star projection `q` when `q * p = p`. -/
theorem le_of_mul_eq_right (hp : IsStarProjection p) (hq : IsStarProjection q)
    (hpq : q * p = p) : p ≤ q := sub_nonneg.mp (hp.sub_of_mul_eq_right hq hpq).nonneg

end NonUnitalRing

end IsStarProjection
